es:event_system{i:l}, a,b:es-E(es).
((es-first(es; a)))
 ((es-first(es; b)))
 (es-pred(es; a) = es-pred(es; b)  es-E(es))
 (a = b) 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), P  Q, P  Q, es-le(es; e; e'), P  Q, True, T, event_system{i:l}, loc(e), Id, es-first(es; e), b, es-pred(es; e), prop{i:l}, es-locl(es; e; e'), es-E(es), P  Q
Lemmas	es-pred wf, not wf, assert wf, es-first wf, es-axioms, es-loc-pred, Id wf, es-loc wf, squash wf, true wf, es-E wf, event system wf, es-le wf, es-le-pred, es-locl-antireflexive